Model: | ftwc v.3 (MA) |
Parameter(s) | N = 8, TIME_BOUND = 5 |
Property: | TimeMin (exp-time) |
mcsta/modest mcsta ftwc.jani -E N=8,TIME_BOUND=5 --props TimeMin -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --epsilon 0 --absolute-epsilon
Walltime: | 464.5924286842346s |
Return code: | 0 |
Note(s): | The tool result '4988349398329471/2500000000' is tagged as incorrect. The reference result is '49569188244691157640777897241488668673626828644189196764038763495934127772581818827657586026182066161989586432749290712194700462126341074934150546100723871655022185670368170152617720178361433722295645619967358084478494099834546378515936142056456021598789834283048399401085339317779160390335682147332083362300224412076816495866312174143937455974191483876650634293062037795776270685493296644510209669509237851584765684566319405462211776204286741525848384633073583969430572762424515151621071750667235423403758187586317061236078533181354878564558387588980534648853069632194739724249745082550820673689600851494125098336522102029348889315394356316567042690867241625261321753876969463822917919195565785841792738462060644802994850536051247180583737651569809934874977339480766075664244250332086771357685540617282828501673946775997764669305736487039689172341089365623671489365717826320627382322103417725112433594282348889076090944230945406554918527903586582075043048674014511775664428763679569460522578957195093204969068885918475954701981402654127272466212590205273467564862315724959246929444124634711891552506708340148443800560671281541666269819810615151079332224771479495605749007741738092305482664765071171188083874586957347417508650944279607451563868631260391999681051953256273570589614525154845090948500816094914209009712314266308932240145318038518254540637911577676498155054493673673322363318272452913909409954810049120798288862526997108335418019182140484143216503177367680163525695647392660591226665498917649041525209344406718195961721470760740289700558365483413406314301238058452518910989373505461571250706410608116754534657620512043545742686327075556074969531847055414282142342990587271158113524384810692830321875392616737551359026591315526253863159107359791046537161916908190887590221726345491223571497457986130346683481045292688213449727577039326510222012881402702075807120/24842480089988447240790617968641731326940011285882082728179896138423523367936760021370104561829991319957969724182256554425167446318631445950695892190402200836787387825155296486116781062019218601643410100142338505175042674102424627326985770121516822573795411953828822495761575522151561445549403085550785674313461919668355506791088789501834828697680745307151308323681304495965293483776759303307260636277363175284409815738275729579884513414133969667756339462005963610505631087075363687809962404734200149292991785208958801489793636767017334885872786774677826308936498950592119270646451579725797475568214721614617543921340306589538760150278878465396260176691820614575734157703329470399589957386076277139682713044193347334676400310427293961340032044853283332077959111706619134528827537788327134939782541587456360768634523647132311813576410650991163357018897462476294723921890820274571494991217501269601816908351375125936826784571099088551243742036837407584471455136531016695810076672064640322257880612919897434991437719737996503119899441329003804923403751422819820661775082756378482159004005829507361729274693612684741636552544024653448109238047025949136815529375658991993266253110622081321025838624126453055551758039028171267383158887476201289629124095280666902919443923213711890766831606926524195878661782192061815893415105317562221779731297712719333522448927790537703584926982226192215421677660470272113138984504066019788276425859009119389029354552006489918430035857810365628253511760413105497853130919105042626582736098208254848720104572120600608729116426288869899829856901833423746811338914270544621210968972627535306289365445761466299769041279947528407598940212566703547006078502616697208674580830606531520061155353505169548249135604202264576558988956723219864209825965891779696849654064191030724636930430924643971545682008428417071282354575536083253622140884212063927' (approx. 1995339.7593611279) which means a relative error of '1.470397872701635e-11' which is larger than the goal precision '1e-14'. |
Relative Error: | 1.470397872701635e-11 |
ftwc.jani:model: info: ftwc is an MA model. ftwc.jani: info: Need at least 40 bytes per state. ftwc.jani: info: Explored 10299 states for N=8, TIME_BOUND=5. ftwc.jani:properties[3]: warning: Computing minimum expected reward in property "TimeMin" without checking for zero-reward end components. Peak memory usage: 59 MB Analysis results for ftwc.jani Experiment N=8, TIME_BOUND=5 + State space exploration Min. state size: 40 bytes States: 10299 Transitions: 12635 Branches: 26983 Rate: 74094 states/s Time: 0.1 s + Property TimeMin Value: 1995339.7593317884 Bounds: [1995339.7593317884, infinity) Time: 463.9 s + Precomputations Max. prob. 1 states: 10299 Time for max. prob. 1 states: 0.0 s + Essential states Iterations: 3 Essential states: 5205 Transitions: 7541 Branches: 21889 Time: 0.0 s + Value iteration Final error: 0 Iterations: 1625839 Time: 463.9 s Exported results to file "/out.txt".
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.